nat(0).
nat(succ(X)):-nat(X).
plus(X, 0, X):-nat(X).
plus(X, succ(Y), succ(Z)):-plus(X, Y, Z).
